Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    flatten(nil)  → nil
2:    flatten(unit(x))  → flatten(x)
3:    flatten(x ++ y)  → flatten(x) ++ flatten(y)
4:    flatten(unit(x) ++ y)  → flatten(x) ++ flatten(y)
5:    flatten(flatten(x))  → flatten(x)
6:    rev(nil)  → nil
7:    rev(unit(x))  → unit(x)
8:    rev(x ++ y)  → rev(y) ++ rev(x)
9:    rev(rev(x))  → x
10:    x ++ nil  → x
11:    nil ++ y  → y
12:    (x ++ y) ++ z  → x ++ (y ++ z)
There are 12 dependency pairs:
13:    FLATTEN(unit(x))  → FLATTEN(x)
14:    FLATTEN(x ++ y)  → flatten(x) ++# flatten(y)
15:    FLATTEN(x ++ y)  → FLATTEN(x)
16:    FLATTEN(x ++ y)  → FLATTEN(y)
17:    FLATTEN(unit(x) ++ y)  → flatten(x) ++# flatten(y)
18:    FLATTEN(unit(x) ++ y)  → FLATTEN(x)
19:    FLATTEN(unit(x) ++ y)  → FLATTEN(y)
20:    REV(x ++ y)  → rev(y) ++# rev(x)
21:    REV(x ++ y)  → REV(y)
22:    REV(x ++ y)  → REV(x)
23:    (x ++ y) ++# z  → x ++# (y ++ z)
24:    (x ++ y) ++# z  → y ++# z
The approximated dependency graph contains 3 SCCs: {23,24}, {13,15,16,18,19} and {21,22}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 3, 2006